w:world{i:l}.
(i:Id, t:, l:IdLnk. isrcv(l;a(i;t))  destination(l) = i)
 w-machine-constraint(w)  Prop{i'} 

latex

Definitions

False, P  Q, A, t  T, x:A. B(x), a(i;t), kind(a), isrcv(k), left+right, P  Q, Dec(P), b, AB, , {x:A| B(x) }, , b, x:AB(x), x:AB(x), P & Q, P  Q, tag(k), lnk(k), w.M, f(a), , s = t, Prop, act(k), w.TA, islocal(k), Unit, kindcase(k; a.f(a); l,t.g(l;t) ), valtype(i;a), Type, val(a), S  T, Msg(M), IdLnk, Id, s(i;t).x, #$n, vartype(i;x), w.T, n+m, a<b, Void, type List, x.A(x), mlnk(m), source(l), m(i;t), outl(x), isl(x), A & B, S  T, isnull(a), let x,y,z = a in t(x;y;z), w-automaton(T;TA;M), w-machine(w;i), World, destination(l), isrcv(l;a), w-machine-constraint(w)

Lemmas

w-isrcvl wf, ldst wf, world wf, w-machine wf, w-automaton wf, nat wf, w-isnull wf, w-T wf, isl wf, outl wf, w-valtype wf, unit wf, w-m wf, lsrc wf, mlnk wf, Msg wf, IdLnk wf, Id wf, le wf, w-vartype wf, w-s wf, w-val wf, eqtt to assert, iff transitivity, eqff to assert, islocal wf, w-TA wf, actof wf, bool wf, subtype rel self, w-M wf, lnk wf, tagof wf, islocal-not-isrcv, not functionality wrt iff, assert of bnot, bnot wf, not wf, assert wf, decidable assert, isrcv wf, w-kind wf, w-a wf